FDL - Step of Proof: and_functionality_wrt

Step of Proof: and_functionality_wrt_implies

9,38

Inference at *
Iof proof for Lemma and functionality wrt implies:

P1,P2,Q1,Q2:

. {P1

P2}

{Q1

Q2}

{(P1

Q1)

(P2

Q2)}

by ((((Unfold `guard` 0)

CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n

C)) (first_tok :t) inil_term)))

)

CollapseTHEN (HypBackchain))

Definitions t T, P Q, {T}, P Q, , x:A. B(x)